Bounded analysis improvements, CLI bindings for CFA,STS,XSTS #286

mondokm · 2024-07-31T10:01:45Z

This PR adds the following:

Removed redundancy between MonolithicExpr and MonolithicTransFunc
BMC, Kind, IMC command line bindings for CFA, STS, XSTS
Unified toMonolithicExpr transformation function for all formalisms
Unified valToState and biValToAction for all formalisms
Introduced initial offset indexing into MonolithicExpr, adjusted BoundedChecker
Minor fixes

…ses to MonolithicExpr

sonarcloud · 2024-07-31T11:44:30Z

Quality Gate failed

Failed conditions
4.2% Coverage on New Code (required ≥ 60%)
5.0% Duplication on New Code (required ≤ 5%)

See analysis details on SonarCloud

github-actions · 2024-07-31T11:59:16Z

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

✅ ConcurrencySafety-Main (3 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ConcurrencySafety-Main, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:48:51 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1427-249
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.222 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ConcurrencySafety-Main
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                     status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------
pthread-ext/18_read_write_lock-pthread.yml    Parsing OK                      10.13        5.03        None
pthread-atomic/read_write_lock-1.yml          true                            11.19        4.23        None
pthread-wmm/rfi003_tso.yml                    TIMEOUT                        120.79       88.89        None
pthread/lazy01.yml                            false(unreach-call)              8.11        3.43        None
pthread-wmm/mix000.oepc.yml                   false(unreach-call)             19.95        7.53        None
-----------------------------------------------------------------------------------------------------------
Run set 1                                     done                            49.47      109.85           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               3
    correct true:        1
    correct false:       2
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               2
  Score:                 4 (max: 8)

✅ ConcurrencySafety-MemSafety (4 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety
date:                    Wed, 2024-07-31 11:48:37 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az573-810
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.3 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call
Run set 1 of 4: skipped because it has no files


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety
Run set 4 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                     status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------
pthread-ext/18_read_write_lock-pthread.yml    Parsing OK                      10.09        5.01        None
pthread-atomic/read_write_lock-1.yml          true                             8.47        3.39        None
pthread-wmm/rfi003_tso.yml                    true                            14.90        6.04        None
pthread/lazy01.yml                            true                             7.16        3.07        None
pthread-wmm/mix000.oepc.yml                   true                            13.58        5.64        None
-----------------------------------------------------------------------------------------------------------
Run set 4                                     done                            54.18       23.68           -

Statistics:              5 Files
  correct:               4
    correct true:        4
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               1
  Score:                 8 (max: 10)

✅ ConcurrencySafety-NoOverflows (4 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call, SV-COMP24_no-data-race, SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:48:39 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1382-274
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.193 MHz
ram:                     16757.338112 MB
------------------------------------------------------------



SV-COMP24_unreach-call
Run set 1 of 4: skipped because it has no files


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows
Run set 3 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                     status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------
pthread-ext/18_read_write_lock-pthread.yml    Parsing OK                      11.62        5.43        None
pthread-atomic/read_write_lock-1.yml          true                             9.19        3.64        None
pthread-wmm/rfi003_tso.yml                    true                            15.06        6.42        None
pthread/lazy01.yml                            true                             7.97        3.32        None
pthread-wmm/mix000.oepc.yml                   true                            14.95        6.14        None
-----------------------------------------------------------------------------------------------------------
Run set 3                                     done                            58.76       25.47           -


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               4
    correct true:        4
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               1
  Score:                 8 (max: 10)

✅ NoDataRace-Main (4 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call, SV-COMP24_no-data-race.NoDataRace-Main, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:48:55 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az801-433
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3239.951 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call
Run set 1 of 4: skipped because it has no files


SV-COMP24_no-data-race.NoDataRace-Main
Run set 2 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                     status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------
pthread-ext/18_read_write_lock-pthread.yml    Parsing OK                      10.28        5.10        None
pthread-atomic/read_write_lock-1.yml          true                            11.69        4.38        None
pthread-wmm/rfi003_tso.yml                    true                            18.34        7.05        None
pthread/lazy01.yml                            true                             7.97        3.30        None
pthread-wmm/mix000.oepc.yml                   true                            17.80        7.01        None
-----------------------------------------------------------------------------------------------------------
Run set 2                                     done                            66.04       27.37           -


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               4
    correct true:        4
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               1
  Score:                 8 (max: 10)

✅ ReachSafety-Arrays (1 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-Arrays, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:47:10 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az661-193
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3197.272 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Arrays
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                         status                       cpu time   wall time        host
---------------------------------------------------------------------------------------------------------------
array-examples/standard_partition_ground-2.yml    TIMEOUT                         76.32      161.00        None
array-crafted/mapavg4.yml                         TIMEOUT                         76.77      161.02        None
array-programs/copysome2-1.yml                    TIMEOUT                         78.15      161.02        None
array-examples/sanfoundry_24-1.yml                true                            11.96      103.28        None
array-multidimensional/max-2-u.yml                ERROR (frontend failed)          1.88        0.80        None
---------------------------------------------------------------------------------------------------------------
Run set 1                                         done                            14.18      588.36           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               1
    correct true:        1
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 2 (max: 10)

✅ ReachSafety-BitVectors (3 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-BitVectors, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:46:11 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az564-73
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.016 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-BitVectors
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                      status                       cpu time   wall time        host
------------------------------------------------------------------------------------------------------------
bitvector/gcd_4.yml                            true                             6.60        2.87        None
bitvector/soft_float_1-3a.c.cil.yml            false(unreach-call)             31.90       17.48        None
bitvector-regression/integerpromotion-3.yml    false(unreach-call)              4.99        2.85        None
bitvector/sum02-1.yml                          Parsing OK                      35.70       18.25        None
bitvector-loops/diamond_2-1.yml                TIMEOUT                        120.49      106.07        None
------------------------------------------------------------------------------------------------------------
Run set 1                                      done                            74.22      148.14           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               3
    correct true:        1
    correct false:       2
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               2
  Score:                 4 (max: 6)

❓ ReachSafety-Combinations (0 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-Combinations, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:47:49 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az665-750
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3206.797 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Combinations
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                                status                       cpu time   wall time        host
----------------------------------------------------------------------------------------------------------------------
pc_sfifo_3.cil+token_ring.02.cil-2.yml                   TIMEOUT                        120.74       72.64        None
Problem05_label47+token_ring.02.cil-1.yml                TIMEOUT                        120.31       95.63        None
pc_sfifo_3.cil+token_ring.11.cil-1.yml                   TIMEOUT                        121.06      109.16        None
Problem05_label45+token_ring.01.cil-2.yml                TIMEOUT                        120.36       95.46        None
pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml    TIMEOUT                        120.25       68.14        None
----------------------------------------------------------------------------------------------------------------------
Run set 1                                                done                             0.61      442.05           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 5)

✅ ReachSafety-ControlFlow (1 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-ControlFlow, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:46:19 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1108-493
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3166.66 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-ControlFlow
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                              status                       cpu time   wall time        host
--------------------------------------------------------------------------------------------------------------------
longjmp/68-longjmp_18-simple-else_unknown_1_pos.yml    ERROR (frontend failed)          3.21        1.14        None
locks/test_locks_11.yml                                TIMEOUT                        122.86      102.99        None
locks/test_locks_5.yml                                 true                            14.69        5.63        None
longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml    ERROR (frontend failed)          3.63        1.32        None
longjmp/68-longjmp_11-counting-return_true.yml         ERROR (frontend failed)          2.03        0.86        None
--------------------------------------------------------------------------------------------------------------------
Run set 1                                              done                            23.03      112.97           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               1
    correct true:        1
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 2 (max: 8)

❓ ReachSafety-ECA (0 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-ECA, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:49:24 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1153-711
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3037.227 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-ECA
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                              status                       cpu time   wall time        host
----------------------------------------------------------------------------------------------------
eca-rers2012/Problem06_label18.yml     TIMEOUT                        120.54       78.19        None
eca-rers2012/Problem06_label11.yml     TIMEOUT                        120.73       75.02        None
eca-programs/Problem101_label07.yml    TIMEOUT                        120.82       73.30        None
eca-rers2012/Problem05_label44.yml     TIMEOUT                        121.04       73.86        None
eca-rers2012/Problem04_label05.yml     TIMEOUT                        121.11       76.08        None
----------------------------------------------------------------------------------------------------
Run set 1                              done                             0.60      378.98           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 7)

✅ ReachSafety-Floats (4 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-Floats, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:49:06 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1269-474
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.911 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Floats
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                          status                       cpu time   wall time        host
----------------------------------------------------------------------------------------------------------------
float-benchs/float_double.yml                      true                             6.02        2.90        None
float-benchs/zonotope_loose.c.v+cfa-reducer.yml    TIMEOUT                        120.49      111.79        None
float-benchs/float_int_inv_square.yml              false(unreach-call)              6.80        3.34        None
floats-cdfpl/square_3.yml                          false(unreach-call)             88.93       85.01        None
floats-cbmc-regression/float11.yml                 true                             5.58        3.06        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            25.66      207.13           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               4
    correct true:        2
    correct false:       2
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               1
  Score:                 6 (max: 8)

❓ ReachSafety-Hardware (0 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-Hardware, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:49:30 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1385-208
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2873.973 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Hardware
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                            status                       cpu time   wall time        host
------------------------------------------------------------------------------------------------------------------
btor2c-lazyMod.arbitrated_top_n4_w16_d32_e0.yml      TIMEOUT                        120.67      111.47        None
btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml    TIMEOUT                        120.44       99.00        None
btor2c-lazyMod.extinction.4.prop1-func-interl.yml    TIMEOUT                        120.47       94.47        None
btor2c-lazyMod.lup.2.prop1-func-interl.yml           TIMEOUT                        120.47       95.36        None
btor2c-lazyMod.train-gate.6.prop1-func-interl.yml    TIMEOUT                        120.85       82.20        None
------------------------------------------------------------------------------------------------------------------
Run set 1                                            done                             0.60      485.15           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 9)

✅ ReachSafety-Heap (5 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-Heap, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:46:46 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1456-958
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3190.383 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Heap
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                 status                       cpu time   wall time        host
---------------------------------------------------------------------------------------
test09.yml                true                             9.76        4.76        None
test15.yml                true                             8.79        4.41        None
just_assert.yml           true                             5.55        2.87        None
volatile_alias.yml        true                             8.06        4.23        None
mutex_lock_int.c_1.yml    true                             9.21        4.54        None
---------------------------------------------------------------------------------------
Run set 1                 done                            41.34       21.35           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               5
    correct true:        5
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               0
  Score:                10 (max: 10)

✅ ReachSafety-Loops (1 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-Loops, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:48:26 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1245-111
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3255.362 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Loops
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                          status                       cpu time   wall time        host
----------------------------------------------------------------------------------------------------------------
nla-digbench/ps3-ll.yml                            TIMEOUT                        120.50      106.95        None
loop-crafted/simple_vardep_2.yml                   TIMEOUT                        120.82      109.79        None
nla-digbench-scaling/divbin_valuebound100.yml      TIMEOUT                        120.66      107.61        None
nla-digbench-scaling/mannadiv_valuebound50.yml     true                            23.00       10.38        None
nla-digbench-scaling/mannadiv_unwindbound10.yml    Parsing OK                      29.35       12.80        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            52.58      349.17           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               1
    correct true:        1
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 2 (max: 9)

✅ ReachSafety-Recursive (1 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-Recursive, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:46:33 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az735-305
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3235.906 MHz
ram:                     16757.338112 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Recursive
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                           status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------------
recursive-simple/id_o100.yml                        Parsing OK                      17.65        7.38        None
recursive-simple/id2_i5_o5-2.yml                    true                            13.79        5.33        None
recursified_nla-digbench/recursified_geo2-ll.yml    TIMEOUT                         33.42      161.02        None
recursive/recHanoi03-2.yml                          TIMEOUT                        120.35       91.95        None
recursified_nla-digbench/recursified_lcm2.yml       TIMEOUT                        120.37      114.01        None
-----------------------------------------------------------------------------------------------------------------
Run set 1                                           done                            31.76      381.47           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               1
    correct true:        1
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 2 (max: 9)

✅ ReachSafety-Sequentialized (1 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-Sequentialized, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:47:33 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az837-459
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.904 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Sequentialized
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                                         status                       cpu time   wall time        host
-------------------------------------------------------------------------------------------------------------------------------
systemc/transmitter.12.cil.yml                                    TIMEOUT                        120.25      108.78        None
seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml        TIMEOUT                        120.33       94.50        None
systemc/pipeline.cil-1.yml                                        TIMEOUT                        120.22      104.98        None
seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml    TIMEOUT                        120.53       93.84        None
seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml            false(unreach-call)            107.11       68.44        None
-------------------------------------------------------------------------------------------------------------------------------
Run set 1                                                         done                           105.75      471.97           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               1
    correct true:        0
    correct false:       1
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 1 (max: 6)

❓ ReachSafety-XCSP (0 / 0 / 5)

table-generator output: HTML/CSV

   BENCHMARK INFORMATION
benchmark definition:    xml/theta.xml
name:                    theta
run sets:                SV-COMP24_unreach-call.ReachSafety-XCSP, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety
date:                    Wed, 2024-07-31 11:46:19 UTC
tool:                    Theta 6.3.0
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az840-758
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.505 MHz
ram:                     16757.334016 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-XCSP
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                  status                       cpu time   wall time        host
----------------------------------------------------------------------------------------
CostasArray-14.yml         TIMEOUT                        120.37      105.42        None
Dubois-025.yml             TIMEOUT                        120.28      108.20        None
aim-100-2-0-unsat-4.yml    TIMEOUT                        120.23      107.73        None
AllInterval-014.yml        TIMEOUT                        120.11      107.42        None
AllInterval-005.yml        TIMEOUT                        120.91      109.18        None
----------------------------------------------------------------------------------------
Run set 1                  done                             0.60      538.98           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 7)

mondokm requested a review from leventeBajczi July 31, 2024 10:05

mondokm added enhancement Ready to test This will run the final sonar check in PRs. labels Jul 31, 2024

mondokm added 18 commits July 31, 2024 13:30

Remove redundant MonolithicTransFunc interface, adjust converter clas…

5f44e65

…ses to MonolithicExpr

Fixed typos in filenames

ddb92f9

Remove unused file

80d508a

Reformat code

67c2891

Move xcfa to monolithic conversion to match other formalisms

3735869

Enable Kind and IMC based on the solvers provided

f1f4492

Add valToState and biValToAction for CFA

ae9acb6

Add cli bindings for bmc,kind,imc

d724dfa

Add valToState and biValToAction for XSTS

ddf4452

Add sts boundedchecker cli binding

5caab29

Move XstsToMonolithicExpr.kt

687755f

Add BoundedCheckerBuilder.kt

1d4ab24

Make cfa-analysis a kotlin project

71fe85e

Add cli bindings for xsts, use bounded builder in all formalisms

e61b297

Remove moved functions

805793f

Fix bugs in sts,xsts bounded cli bindings

efe5193

Reformat files

a927f6a

Resolve rebase conflict

e407b7b

mondokm force-pushed the monolithic branch from 0b6e163 to e407b7b Compare July 31, 2024 11:31

mondokm merged commit 5c81278 into master Jul 31, 2024
81 of 82 checks passed

mondokm deleted the monolithic branch July 31, 2024 12:05

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Bounded analysis improvements, CLI bindings for CFA,STS,XSTS #286

Bounded analysis improvements, CLI bindings for CFA,STS,XSTS #286

mondokm commented Jul 31, 2024

sonarcloud bot commented Jul 31, 2024

github-actions bot commented Jul 31, 2024

Bounded analysis improvements, CLI bindings for CFA,STS,XSTS #286

Bounded analysis improvements, CLI bindings for CFA,STS,XSTS #286

Conversation

mondokm commented Jul 31, 2024

sonarcloud bot commented Jul 31, 2024

Quality Gate failed

github-actions bot commented Jul 31, 2024